(set-logic QF_AUFBV)
(set-info :source |These benchmarks are derived from a semi-automated proof of functional equivalence between two implementations of an Elliptic Curve Digital Signature Algorithm (ECDSA). More information about problem they encode can be found here: http://cps-vo.org/node/3405|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status sat)
(declare-fun x83 () (_ BitVec 1))
(declare-fun x81 () (_ BitVec 1))
(declare-fun x80 () (_ BitVec 1))
(declare-fun x79 () (Array (_ BitVec 5) (_ BitVec 32)))
(declare-fun x78 () (_ BitVec 32))
(declare-fun x77 () (_ BitVec 64))
(declare-fun x76 () (_ BitVec 64))
(declare-fun x75 () (_ BitVec 64))
(declare-fun x74 () (_ BitVec 32))
(declare-fun x73 () (_ BitVec 64))
(declare-fun x71 () (_ BitVec 1))
(declare-fun x69 () (_ BitVec 1))
(declare-fun x68 () (_ BitVec 1))
(declare-fun x67 () (Array (_ BitVec 5) (_ BitVec 32)))
(declare-fun x66 () (_ BitVec 768))
(declare-fun x65 () (_ BitVec 832))
(declare-fun x64 ((_ BitVec 32) (_ BitVec 768) (_ BitVec 32) (_ BitVec 32) (_ BitVec 32) (_ BitVec 64)) (_ BitVec 832))
(declare-fun x63 () (_ BitVec 768))
(declare-fun x62 () (Array (_ BitVec 5) (_ BitVec 32)))
(declare-fun x61 () (_ BitVec 32))
(declare-fun x60 () (_ BitVec 64))
(declare-fun x59 () (_ BitVec 64))
(declare-fun x58 () (_ BitVec 64))
(declare-fun x57 () (_ BitVec 64))
(declare-fun x56 () (_ BitVec 64))
(declare-fun x55 () (_ BitVec 64))
(declare-fun x54 () (_ BitVec 64))
(declare-fun x52 () (_ BitVec 1))
(declare-fun x50 () (_ BitVec 1))
(declare-fun x49 () (_ BitVec 1))
(declare-fun x47 () (_ BitVec 1))
(declare-fun x45 () (_ BitVec 1))
(declare-fun x43 () (_ BitVec 1))
(declare-fun x42 () (_ BitVec 1))
(declare-fun x40 () (_ BitVec 1))
(declare-fun x39 () (_ BitVec 1))
(declare-fun x37 () (_ BitVec 1))
(declare-fun x36 () (_ BitVec 1))
(declare-fun x34 () (_ BitVec 1))
(declare-fun x32 () (_ BitVec 1))
(declare-fun x31 () (_ BitVec 1))
(declare-fun x29 () (_ BitVec 1))
(declare-fun x28 () (_ BitVec 1))
(declare-fun x26 () (_ BitVec 1))
(declare-fun x25 () (_ BitVec 1))
(declare-fun x23 () (_ BitVec 1))
(declare-fun x21 () (_ BitVec 1))
(declare-fun x20 () (_ BitVec 1))
(declare-fun x18 () (_ BitVec 1))
(declare-fun x17 () (_ BitVec 1))
(declare-fun x15 () (_ BitVec 1))
(declare-fun x13 () (_ BitVec 1))
(declare-fun x12 () (_ BitVec 1))
(declare-fun x10 () (_ BitVec 1))
(declare-fun x8 () (_ BitVec 1))
(declare-fun x7 () (_ BitVec 1))
(declare-fun x6 () (_ BitVec 1))
(declare-fun x5 () (_ BitVec 32))
(declare-fun x4 () (Array (_ BitVec 5) (_ BitVec 32)))
(declare-fun x3 () (_ BitVec 32))
(declare-fun x2 () (_ BitVec 32))
(declare-fun x1 () (_ BitVec 32))
(declare-fun x0 () (_ BitVec 64))
(declare-fun p84 () Bool)
(declare-fun p82 () Bool)
(declare-fun p72 () Bool)
(declare-fun p70 () Bool)
(declare-fun p53 () Bool)
(declare-fun p51 () Bool)
(declare-fun p48 () Bool)
(declare-fun p46 () Bool)
(declare-fun p44 () Bool)
(declare-fun p41 () Bool)
(declare-fun p38 () Bool)
(declare-fun p35 () Bool)
(declare-fun p33 () Bool)
(declare-fun p30 () Bool)
(declare-fun p27 () Bool)
(declare-fun p24 () Bool)
(declare-fun p22 () Bool)
(declare-fun p19 () Bool)
(declare-fun p16 () Bool)
(declare-fun p14 () Bool)
(declare-fun p11 () Bool)
(declare-fun p9 () Bool)
(assert (= p84 (and p70 p82)))
(assert (= x83 (bvand x69 x81)))
(assert (= p82 (or p72 (= x79 x67))))
(assert (= x81 (bvor x71 x80)))
(assert (= x80 (ite (= x79 x67) (_ bv1 1) (_ bv0 1))))
(assert (= x79 (store x4 ((_ extract 4 0) x3) x78)))
(assert (= (select x79 (_ bv31 5)) (_ bv0 32)))
(assert (= (select x79 (_ bv30 5)) (_ bv0 32)))
(assert (= (select x79 (_ bv29 5)) (_ bv0 32)))
(assert (= (select x79 (_ bv28 5)) (_ bv0 32)))
(assert (= (select x79 (_ bv27 5)) (_ bv0 32)))
(assert (= (select x79 (_ bv26 5)) (_ bv0 32)))
(assert (= (select x79 (_ bv25 5)) (_ bv0 32)))
(assert (= (select x79 (_ bv24 5)) (_ bv0 32)))
(assert (= x78 ((_ extract 31 0) x77)))
(assert (= x77 (bvadd x73 x76)))
(assert (= x76 (bvand x75 (_ bv4294967295 64))))
(assert (= x75 ((_ sign_extend 32) x74)))
(assert (= x74 (select x4 ((_ extract 4 0) x3))))
(assert (= x73 (bvadd x0 x58)))
(assert (= p72 (and p19 (bvsle x3 (_ bv23 32)))))
(assert (= x71 (bvand x18 x20)))
(assert (= p70 (or p53 (= x62 x67))))
(assert (= x69 (bvor x52 x68)))
(assert (= x68 (ite (= x62 x67) (_ bv1 1) (_ bv0 1))))
(assert (= (select x67 (_ bv23 5)) ((_ extract 767 736) x66)))
(assert (= (select x67 (_ bv22 5)) ((_ extract 735 704) x66)))
(assert (= (select x67 (_ bv21 5)) ((_ extract 703 672) x66)))
(assert (= (select x67 (_ bv20 5)) ((_ extract 671 640) x66)))
(assert (= (select x67 (_ bv19 5)) ((_ extract 639 608) x66)))
(assert (= (select x67 (_ bv18 5)) ((_ extract 607 576) x66)))
(assert (= (select x67 (_ bv17 5)) ((_ extract 575 544) x66)))
(assert (= (select x67 (_ bv16 5)) ((_ extract 543 512) x66)))
(assert (= (select x67 (_ bv15 5)) ((_ extract 511 480) x66)))
(assert (= (select x67 (_ bv14 5)) ((_ extract 479 448) x66)))
(assert (= (select x67 (_ bv13 5)) ((_ extract 447 416) x66)))
(assert (= (select x67 (_ bv12 5)) ((_ extract 415 384) x66)))
(assert (= (select x67 (_ bv11 5)) ((_ extract 383 352) x66)))
(assert (= (select x67 (_ bv10 5)) ((_ extract 351 320) x66)))
(assert (= (select x67 (_ bv9 5)) ((_ extract 319 288) x66)))
(assert (= (select x67 (_ bv8 5)) ((_ extract 287 256) x66)))
(assert (= (select x67 (_ bv7 5)) ((_ extract 255 224) x66)))
(assert (= (select x67 (_ bv6 5)) ((_ extract 223 192) x66)))
(assert (= (select x67 (_ bv5 5)) ((_ extract 191 160) x66)))
(assert (= (select x67 (_ bv4 5)) ((_ extract 159 128) x66)))
(assert (= (select x67 (_ bv3 5)) ((_ extract 127 96) x66)))
(assert (= (select x67 (_ bv2 5)) ((_ extract 95 64) x66)))
(assert (= (select x67 (_ bv1 5)) ((_ extract 63 32) x66)))
(assert (= (select x67 (_ bv0 5)) ((_ extract 31 0) x66)))
(assert (= (select x67 (_ bv31 5)) (_ bv0 32)))
(assert (= (select x67 (_ bv30 5)) (_ bv0 32)))
(assert (= (select x67 (_ bv29 5)) (_ bv0 32)))
(assert (= (select x67 (_ bv28 5)) (_ bv0 32)))
(assert (= (select x67 (_ bv27 5)) (_ bv0 32)))
(assert (= (select x67 (_ bv26 5)) (_ bv0 32)))
(assert (= (select x67 (_ bv25 5)) (_ bv0 32)))
(assert (= (select x67 (_ bv24 5)) (_ bv0 32)))
(assert (= x66 ((_ extract 767 0) x65)))
(assert (= x65 (x64 x5 x63 x3 x2 x1 x0)))
(assert (= x63 (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (select x4 (_ bv23 5)) (select x4 (_ bv22 5))) (select x4 (_ bv21 5))) (select x4 (_ bv20 5))) (select x4 (_ bv19 5))) (select x4 (_ bv18 5))) (select x4 (_ bv17 5))) (select x4 (_ bv16 5))) (select x4 (_ bv15 5))) (select x4 (_ bv14 5))) (select x4 (_ bv13 5))) (select x4 (_ bv12 5))) (select x4 (_ bv11 5))) (select x4 (_ bv10 5))) (select x4 (_ bv9 5))) (select x4 (_ bv8 5))) (select x4 (_ bv7 5))) (select x4 (_ bv6 5))) (select x4 (_ bv5 5))) (select x4 (_ bv4 5))) (select x4 (_ bv3 5))) (select x4 (_ bv2 5))) (select x4 (_ bv1 5))) (select x4 (_ bv0 5)))))
(assert (= x62 (store x4 ((_ extract 4 0) x3) x61)))
(assert (= (select x62 (_ bv31 5)) (_ bv0 32)))
(assert (= (select x62 (_ bv30 5)) (_ bv0 32)))
(assert (= (select x62 (_ bv29 5)) (_ bv0 32)))
(assert (= (select x62 (_ bv28 5)) (_ bv0 32)))
(assert (= (select x62 (_ bv27 5)) (_ bv0 32)))
(assert (= (select x62 (_ bv26 5)) (_ bv0 32)))
(assert (= (select x62 (_ bv25 5)) (_ bv0 32)))
(assert (= (select x62 (_ bv24 5)) (_ bv0 32)))
(assert (= x61 ((_ extract 31 0) x60)))
(assert (= x60 (bvadd x59 (_ bv0 64))))
(assert (= x59 (bvadd x0 x58)))
(assert (= x58 (bvmul x55 x57)))
(assert (= x57 (bvand x56 (_ bv4294967295 64))))
(assert (= x56 ((_ sign_extend 32) x1)))
(assert (= x55 (bvand x54 (_ bv4294967295 64))))
(assert (= x54 ((_ sign_extend 32) x2)))
(assert (= p53 (or p48 p51)))
(assert (= x52 (bvor x47 x50)))
(assert (= p51 (not (bvsle x3 (_ bv23 32)))))
(assert (= x50 (bvnot x49)))
(assert (= x49 (ite (bvsle x3 (_ bv23 32)) (_ bv1 1) (_ bv0 1))))
(assert (= p48 (or p44 p46)))
(assert (= x47 (bvor x43 x45)))
(assert (= p46 (not (bvsle (_ bv0 32) x3))))
(assert (= x45 (bvnot x36)))
(assert (= p44 (or p41 (= x5 (_ bv0 32)))))
(assert (= x43 (bvor x40 x42)))
(assert (= x42 (ite (= x5 (_ bv0 32)) (_ bv1 1) (_ bv0 1))))
(assert (= p41 (or p38 (bvsle (_ bv24 32) x3))))
(assert (= x40 (bvor x37 x39)))
(assert (= x39 (ite (bvsle (_ bv24 32) x3) (_ bv1 1) (_ bv0 1))))
(assert (= p38 (not (bvsle (_ bv0 32) x3))))
(assert (= x37 (bvnot x36)))
(assert (= x36 (ite (bvsle (_ bv0 32) x3) (_ bv1 1) (_ bv0 1))))
(assert (= p35 (or p22 p33)))
(assert (= x34 (bvor x21 x32)))
(assert (= p33 (and p30 (bvsle x3 (_ bv23 32)))))
(assert (= x32 (bvand x29 x31)))
(assert (= x31 (ite (bvsle x3 (_ bv23 32)) (_ bv1 1) (_ bv0 1))))
(assert (= p30 (and p27 (bvsle (_ bv0 32) x3))))
(assert (= x29 (bvand x26 x28)))
(assert (= x28 (ite (bvsle (_ bv0 32) x3) (_ bv1 1) (_ bv0 1))))
(assert (= p27 (and p24 (= x5 (_ bv0 32)))))
(assert (= x26 (bvand x23 x25)))
(assert (= x25 (ite (= x5 (_ bv0 32)) (_ bv1 1) (_ bv0 1))))
(assert (= p24 (and (bvsle (_ bv0 32) x3) p9)))
(assert (= x23 (bvand x6 x8)))
(assert (= p22 (and p19 (bvsle x3 (_ bv23 32)))))
(assert (= x21 (bvand x18 x20)))
(assert (= x20 (ite (bvsle x3 (_ bv23 32)) (_ bv1 1) (_ bv0 1))))
(assert (= p19 (and p16 (bvsle (_ bv0 32) x3))))
(assert (= x18 (bvand x15 x17)))
(assert (= x17 (ite (bvsle (_ bv0 32) x3) (_ bv1 1) (_ bv0 1))))
(assert (= p16 (and p11 p14)))
(assert (= x15 (bvand x10 x13)))
(assert (= p14 (not (= x5 (_ bv0 32)))))
(assert (= x13 (bvnot x12)))
(assert (= x12 (ite (= x5 (_ bv0 32)) (_ bv1 1) (_ bv0 1))))
(assert (= p11 (and (bvsle (_ bv0 32) x3) p9)))
(assert (= x10 (bvand x6 x8)))
(assert (= p9 (not (bvsle (_ bv24 32) x3))))
(assert (= x8 (bvnot x7)))
(assert (= x7 (ite (bvsle (_ bv24 32) x3) (_ bv1 1) (_ bv0 1))))
(assert (= x6 (ite (bvsle (_ bv0 32) x3) (_ bv1 1) (_ bv0 1))))
(assert true)
(assert (= (select x4 (_ bv31 5)) (_ bv0 32)))
(assert (= (select x4 (_ bv30 5)) (_ bv0 32)))
(assert (= (select x4 (_ bv29 5)) (_ bv0 32)))
(assert (= (select x4 (_ bv28 5)) (_ bv0 32)))
(assert (= (select x4 (_ bv27 5)) (_ bv0 32)))
(assert (= (select x4 (_ bv26 5)) (_ bv0 32)))
(assert (= (select x4 (_ bv25 5)) (_ bv0 32)))
(assert (= (select x4 (_ bv24 5)) (_ bv0 32)))
(assert (not (=> p35 p84)))
(check-sat)
(set-option :regular-output-channel "/dev/null")
(get-model)
(exit)
